Metamath Blueprint : AKS (PRIMES is in P)

Status:

Statement:

$e |- ( ph -> P e. NN ) $.
$e |- ( ph -> R e. NN ) $.
$e |- I = ( P INTRO R ) $.
$e |- ( ph -> E e. NN ) $.
$e |- ( ph -> D e. NN ) $.
$e |- A = ( Base ` ( poly1 ` ZZ ) ) $.
$e |- ( ph -> F e. A ) $.
$e |- ( ph -> D I F ) $.
$e |- ( ph -> E I F ) $.
$p |- ( ph -> ( D x. E ) I F ) $.